Termination Proof Script

Consider the TRS R consisting of the rewrite rules


1:		f(x,y,z)	→ g(x ≤ y,x,y,z)
2:		g(true,x,y,z)	→ z
3:		g(false,x,y,z)	→ f(f(p(x),y,z),f(p(y),z,x),f(p(z),x,y))
4:		p(0)	→ 0
5:		p(s(x))	→ x

There are 8 dependency pairs:


6:		F(x,y,z)	→ G(x ≤ y,x,y,z)
7:		G(false,x,y,z)	→ F(f(p(x),y,z),f(p(y),z,x),f(p(z),x,y))
8:		G(false,x,y,z)	→ F(p(x),y,z)
9:		G(false,x,y,z)	→ P(x)
10:		G(false,x,y,z)	→ F(p(y),z,x)
11:		G(false,x,y,z)	→ P(y)
12:		G(false,x,y,z)	→ F(p(z),x,y)
13:		G(false,x,y,z)	→ P(z)

The approximated dependency graph contains no SCCs and hence the TRS is trivially terminating.

Tyrolean Termination Tool (0.01 seconds) --- May 4, 2006